Nuprl Lemma : unzip_zip
4,23
postcript
pdf
T1
,
T2
:Type,
as
:
T1
List,
bs
:
T2
List. ||
as
|| = ||
bs
||
unzip(zip(
as
;
bs
)) = <
as
,
bs
>
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
||
as
||
,
Prop
,
P
Q
,
i
j
,
unzip(
as
)
Lemmas
non
neg
length
,
length
wf1
origin
T1, T2:Type, as:T1 List, bs:T2 List. ||as|| = ||bs|| 
unzip(zip(as;bs)) = <as,bs> T1, T2:Type, as:T1 List, bs:T2 List. ||as|| = ||bs|| unzip(zip(as;bs)) = <as,bs> Tx:A. B(x) Q
j